i:Id, k:Knd, L:Id List. @i: k writes only members of L ||- es.@i: k affects only L 

latex

Definitions	es realizer ind Raframe compseq tag def, Consistent(R;es), ES, t  T, x:A. B(x), @loc: k writes only members of L, @i: k affects only L, x:AB(x), P  Q, True, R-Feasible(R), inr(x), x:AB(x), P & Q, R ||- es.P(es), Id, Knd, type List
Lemmas	Knd wf, Id wf, R-consistent wf, Raframe wf, event system wf